\begin{tabbing}
$\forall$\=$A$:Type, $B$:($A$$\rightarrow$Type), $f$:$a$:$A$ fp$\rightarrow$ $B$($a$), ${\it eq}$:EqDecider($A$), $x$:$A$,\+
\\[0ex]$P$:($a$:\{$a$:$A$$\mid$ $\uparrow$$a$ $\in$ dom($f$)\} $\rightarrow$$B$($a$)$\rightarrow\mathbb{P}$).
\-\\[0ex]($z$ != $f$($x$) $\Rightarrow$ $P$($x$,$z$)) $\in$ $\mathbb{P}$
\end{tabbing}